$\forall$$x$:Id, $t$:Type, $v$:$t$. AtomFree(Type;$t$) $\Rightarrow$ Feasible($x$ : $t$ initially $x$ = $v$)